\subsection{Introduction to independence results}
Independence results are found across mathematical disciplines.
\begin{enumerate}
    \item The \emph{parallel postulate} is independent from the other four postulates of Euclidean geometry.
    It states that for any given point not on a line, there is a unique line passing through that point that does not intersect the given line.
    In the 19th century, it was shown that the other four postulates are satisfied by hyperbolic geometry, but this postulate is not satisfied.
    This shows that the other four axioms are insufficient to prove the parallel postulate.
    \item Let \( \varphi \) be the statement in the language of fields describing the existence of a square root of 2.
    We know that \( \mathbb Q \) is a field satisfying \( \neg\varphi \), and \( \mathbb Q[\sqrt{2}] \) satisfies \( \varphi \).
    The fields \( \mathbb Q \) and \( \mathbb Q[\sqrt{2}] \) are models of the theory of fields, one of which satisfies \( \varphi \), and one of which satisfies \( \neg\varphi \).
    This shows that the theory of fields does not prove \( \varphi \) or \( \neg\varphi \).
    A similar result holds for the statement \( \varphi \) that says that there are no roots of \( x^4 = -1 \).
    \item G\"odel's incompleteness theorem implies that there must always be an independence result in a sufficiently powerful consistent set theory.
\end{enumerate}
We will show that there are other independence results in set theory that are not self-referential like the G\"odel incompleteness theorems.
\begin{theorem}[Cantor]
    \( \abs{\mathbb N} < \abs{\mathcal P(\mathbb N)} \).
\end{theorem}
The continuum hypothesis is that there are no sets of cardinality strictly between \( \abs{\mathbb N} \) and \( \abs{\mathcal P(N)} = \abs{\mathbb R} \).
\begin{definition}
    The \emph{continuum hypothesis} \( \mathsf{CH} \) states that if \( X \subseteq \mathbb P(\mathbb N) \) is infinite, then either \( \abs{X} = \abs{\mathbb N} \) or \( \abs{X} = \abs{\mathcal P(\mathbb N)} \), or equivalently,
    \[ 2^{\aleph_0} = \aleph_1 \]
\end{definition}
Progress was made on the continuum hypothesis in the 19th and 20th centuries.
\begin{enumerate}
    \item In 1883, Cantor showed that any closed subset of \( \mathbb R \) satisfies \( \mathsf{CH} \).
    \item In 1916, Alexandrov and Hausdorff showed that any Borel set of \( \mathbb R \) satisfies \( \mathsf{CH} \).
    \item In 1930, Suslin strengthened this result to analytic subsets of \( \mathbb R \).
    \item In 1938, G\"odel showed that if \( \mathsf{ZF} \) is consistent, then so is \( \mathsf{ZFC} + \mathsf{CH} \).
    \item However, in 1963, Cohen showed that if \( \mathsf{ZF} \) is consistent, then so is \( \mathsf{ZFC} + \neg\mathsf{CH} \).
\end{enumerate}
In this course, we will prove results (iv) and (v), thus establishing the independence of the continuum hypothesis from \( \mathsf{ZFC} \).

\subsection{Systems of set theory}
The language of set theory \( \mathcal L = \mathcal L_\in \) is a first-order predicate logic with equality and membership as primitive relations.
We assume the existence of infinitely many variables \( v_1, v_2, \dots \) denoting sets.
We will only use the logical connectives \( \vee \) and \( \neg \) as well as the existential quantifier \( \exists \).
Conjunction, implication, and universal quantification can be defined in terms of disjunction, negation, and existential quantification.

We say that an occurrence of a variable \( x \) is \emph{bound} in a formula \( \varphi \) if is in a quantifier \( \exists x \) or lies in the scope of such a quantifier.
An occurrence is called \emph{free} if it is not bound.
We write \( \mathrm{FV}(\varphi) \) for the set of free variables of \( \varphi \).
We will write \( \varphi(u_1, \dots, u_n) \) to emphasise the dependence of \( \varphi \) on its free variables \( u_1, \dots, u_n \).
By doing so, we will allow ourselves to freely change the names of the free variables, and assume that substituted variables are free.
The syntax \( \varphi(u_0, \dots, u_n) \) does not imply that \( u_i \) occurs freely, or even at all.

Some of the most common axioms of set theory are as follows.
\begin{enumerate}
    \item \emph{Axiom of extensionality.}
    \[ \forall x.\, \forall y.\, (\forall z.\, (z \in x \leftrightarrow x \in y) \to x = y) \]
    \item \emph{Axiom of empty set.}
    \[ \exists x.\, \forall y \in x.\, y \neq y \]
    \item \emph{Axiom of pairing.}
    \[ \forall x.\, \forall y.\, \exists z.\, (x \in z \wedge y \in z) \]
    \item \emph{Axiom of union.}
    \[ \forall a.\, \exists x.\, \forall y.\, (y \in x \leftrightarrow \exists z \in a.\, y \in z) \]
    \item \emph{Axiom of foundation.}
    \[ \forall x.\, (\exists y.\, y \in x \to \exists y \in x.\, \neg\exists z \in x.\, z \in y) \]
    \item \emph{Axiom scheme of separation.} For any formula \( \varphi \),
    \[ \forall a.\, \exists x.\, \forall y.\, (y \in x \leftrightarrow (y \in a \wedge \varphi(y))) \]
    \item \emph{Axiom of infinity.}
    \[ \exists a.\, (\exists x.\, (x \in a) \wedge \forall x \in a.\, \exists y \in a.\, x \in y) \]
    \item \emph{Axiom of power set.}
    \[ \forall a.\, \exists x.\, \forall y.\, (y \in x \leftrightarrow \forall z.\, (z \in y \to z \in a)) \]
    \item \emph{Axiom scheme of replacement.} For any formula \( \varphi \),
    \[ \forall a.\, (\forall x \in a.\, \exists! y.\, \varphi(x, y) \to \exists b.\, \forall x \in a.\, \exists y \in b.\, \varphi(x, y)) \]
    \item[(ix\('\))] \emph{Axiom scheme of collection.} For any formula \( \varphi \),
    \[ \forall a.\, (\forall x \in a.\, \exists y.\, \varphi(x, y) \to \exists b.\, \forall x \in a.\, \exists y \in b.\, \varphi(x, y)) \]
    \item \emph{Axiom of choice.}
    \[ \forall X.\, \qty(\varnothing \notin X \to \exists f : \qty(X \to \bigcup X).\, \forall a \in X.\, f(a) \in a) \]
    \item[(x\('\))] \emph{Well-ordering principle.}
    \[ \forall a.\, \exists R.\, R \text{ is a well-ordering of } a \]
\end{enumerate}
Some common set theories are as follows.
\begin{itemize}
    \item \emph{Zermelo set theory} \( \mathsf{Z} \) consists of axioms (i) to (viii).
    Axioms (ix) and (ix\('\)) are equivalent relative to \( \mathsf{Z} \).
    \item \emph{Zermelo--Fraenkel set theory} \( \mathsf{ZF} \) consists of axioms (i) to (ix).
    Axioms (x) and (x\('\)) are equivalent relative to \( \mathsf{ZF} \).
    \item \emph{Zermelo--Fraenkel set theory with choice} \( \mathsf{ZFC} \) consists of axioms (i) to (x).
    \item \emph{Zermelo--Fraenkel set theory without power set} \( \mathsf{ZF}^- \) consists of axioms (i) to (vii), with the axiom of collection (ix\('\)) instead of replacement (ix); it has been shown that (ix) is weaker than (ix\('\)) in the presence of axioms (i) to (vii).
    \item \emph{Zermelo--Fraenkel set theory with choice and without power set} \( \mathsf{ZFC}^- \) consists of axioms (i) to (vii), with the axiom of collection (ix\('\)) and the well-ordering principle (x\('\)).
\end{itemize}
In this course, our main metatheory will be \( \mathsf{ZF} \), and we will be explicit about the use of choice.

We say that a class \( X \) is \emph{definable} over \( M \) if there exists a formula \( \varphi \) and sets \( a_1, \dots, a_n \in M \) such that for all \( z \in M \), we have \( z \in X \) if and only if \( \varphi(z, a_1, \dots, a_n) \).
A class is \emph{proper} over \( M \) if it is not a set in \( M \).

Under suitable hypotheses, there is a countable transitive model \( M \) of \( \mathsf{ZFC} \).
In this case, \( \abs{\mathbb R \cap M} \) is countable, so there exists a real \( v \) that is not in \( M \).
Hence, \( v \) is a proper class over \( M \).
However, it is not definable, and we cannot `talk about it' in the language of set theory.
The only proper classes that affect our theory are the definable ones.

In this course, we will assume that all mentioned classes are definable.
We can then use formulas of the form
\[ \exists C.\, (C \text{ is a class} \wedge \forall x \in C.\, \varphi) \]
by defining it to mean that there is a formula \( \theta \) giving a class \( C \) satisfying \( \forall x \in C.\, \varphi \).
For example, the universe class \( \mathrm{V} = \qty{x \mid x = x} \), the Russell class \( R = \qty{x \mid x \notin x} \), and the class of ordinals are all definable.
Any set is a definable class.
Classes are heavily dependent on the underlying model: if \( M = 2 \) then \( \mathrm{Ord} = 2 = M \), and if \( M = 3 \cup \qty{1} \) then \( \mathrm{Ord} = 3 \neq M \).

Suppose that \( M \) is a set model of \( \mathsf{ZF} \); that is, \( M \) is a set.
Let \( \mathcal D \) be the collection of definable classes over \( M \).
Then one can show that \( \mathcal D \) is a set in our metatheoretic universe \( \mathrm{V} \), and \( (M, \mathcal D) \) is a model of a second-order version of \( \mathsf{ZF} \), known as \emph{G\"odel--Bernays set theory}.

\subsection{Adding defined functions}
Often in set theory, we use symbols such as \( 0, 1, \subseteq, \cap, \wedge, \forall \); they do not exist in our language.
\begin{definition}
    Suppose that \( \mathcal L \subseteq \mathcal L' \) and \( T \) is a set of sentences in \( \mathcal L \).
    We say that \( P \) is a \emph{defined \( n \)-ary predicate} symbol over \( T \) if there is a formula \( \varphi \) in \( \mathcal L \) such that
    \[ T \vdash \forall x_1, \dots, x_n.\, (P(x_1, \dots, x_n) \leftrightarrow \varphi(x_1, \dots, x_n)) \]
    Similarly, we say that \( f \) is a \emph{defined \( n \)-ary function} symbol over \( T \) if there is a formula \( \varphi \) in \( \mathcal L \) such that
    \[ f(x_1, \dots, x_n) = y \text{ if and only if } T \vdash \varphi(x_1, \dots, x_n, y) \]
    and
    \[ T \vdash \forall x_1, \dots, x_n.\, \exists! y.\, \varphi(x_1, \dots, x_n, y) \]
    We say that a set of sentences \( T' \) of \( \mathcal L' \) is an \emph{extension by definitions} of \( T \) over \( \mathcal L \) when \( T' = T \cup S \) and \( S = \qty{\varphi_s \mid s \in \mathcal L' \setminus \mathcal L'} \) and each \( \varphi_s \) is a definition of \( s \) in the language \( \mathcal L \) over \( T \).
\end{definition}
Commonly used symbols such as \( 0, 1, \subseteq, \cap, \mathcal P, \bigcup \) are defined over \( \mathsf{ZF} \).
\begin{theorem}
    Suppose that \( \mathcal L \subseteq \mathcal L' \), and that \( T \) is a set of \( \mathcal L \)-sentences and \( T' \) is an extension by definitions of \( T \) to \( \mathcal L' \).
    Then
    \begin{enumerate}
        \item (conservativity) If \( \varphi \) is a sentence of \( \mathcal L \), then \( T \vdash \varphi \leftrightarrow T' \vdash \varphi \).
        \item (abbreviations) If \( \varphi \) is a formula of \( \mathcal L' \), then there exists a formula \( \hat\varphi \) of \( \mathcal L \) whose free variables are exactly those of \( \varphi \), such that \( T' \vdash \forall x.\, (\varphi \leftrightarrow \hat\varphi) \).
    \end{enumerate}
\end{theorem}
\begin{example}
    The intersection \( a \cap b \) can be defined as the unique set \( c \) such that
    \[ \forall x.\, (x \in c \iff x \in a \wedge x \in b) \]
    This definition makes sense only if there is a unique \( c \) satisfying this formula \( \varphi(c) \).
    If
    \[ M = \qty{a, c, d, \qty{a}, \qty{a, b}, \qty{a, b, c}, \qty{a, b, d}} \]
    then it is easy to check that both \( \qty{a} \) and \( \qty{a, d} \) satisfy \( \varphi \), so intersection cannot be defined.
\end{example}

\subsection{Absoluteness}
It is often the case that definitions appear to give the same set regardless of which model we are working inside.
For example, \( \qty{x \mid x \neq x} \) is the empty set in any model, and \( \qty{x \mid x = a \vee x = b} \) gives a pair set.
Other definitions need not, for example \( \mathcal P(\mathbb N) \), which need not be the true power set in a given transitive model.
To quantify this behaviour, we need to define what it means for \( \varphi \) to hold in an arbitrary structure; this concept is called \emph{relativisation}.
\begin{definition}
    The quantifier \( \forall x \in a.\, \varphi \) is an abbreviation of \( \forall x.\, x \in a \Rightarrow \varphi \).
    We use the analogous abbreviation for the existential quantifier.
    Let \( W \) be a class; we define by recursion the \emph{relativisation} \( \varphi^W \) of \( \varphi \) as follows.
    \begin{align*}
        (x \in y)^W &\equiv x \in y \\
        (x = y)^W &\equiv x = y \\
        (\varphi \vee \psi)^W &\equiv \varphi^W \vee \psi^W \\
        (\neg \varphi)^W &\equiv \neg \varphi^W \\
        (\exists x.\, \varphi)^W &\equiv \exists x \in W.\, \varphi^W
    \end{align*}
\end{definition}
One can easily show that
\begin{align*}
    (\varphi \wedge \psi)^W &\equiv \varphi^W \wedge \psi^W \\
    (\varphi \to \psi)^W &\equiv \varphi^W \to \psi^W \\
    (\forall x.\, \varphi)^W &\equiv \forall x \in W.\, \varphi^W
\end{align*}
\begin{proposition}
    Suppose that \( M \subseteq N \) and \( M \) is a definable class over \( N \).
    Then the relation \( M \vDash \varphi \) is first-order expressible in \( N \).
\end{proposition}
\begin{proof}
    Suppose \( M \) is defined by \( \theta \), so
    \[ \forall z \in N.\, \theta(z) \leftrightarrow z \in M \]
    We claim that \( (N, \in) \vDash \varphi^M \) if and only if \( (M, \in) \vDash \varphi \).
    We proceed by induction on the length of formulae.
    For example,
    \[ N \vDash (x \in y)^M \text{ iff } N \vDash x \in y \text{ and } x, y \in M \text{ iff } \theta(x), \theta(y), M \vDash x \in y \]
    The cases for equality is similar, and disjunction and negation are simple.
    Finally,
    \[ N \vDash (\exists x.\, \varphi(x))^M \text{ iff } N \vDash \exists x.\, x \in M \wedge \varphi^M(x) \]
    which holds precisely when there is some \( x \in N \) such that \( N \vDash x \in M \) and \( N \vDash \varphi^M(x) \), but \( N \vDash x \in M \) if and only if \( \theta(x) \), giving the result as required.
\end{proof}
Thus, relativisation is a way to express truth in definable classes.
\begin{definition}
    Suppose that \( M \subseteq N \) are classes and \( \varphi(u_1, \dots, u_n) \) is a formula.
    Then \( \varphi \) is called
    \begin{enumerate}
        \item \emph{upwards absolute} for \( M, N \) if
        \[ \forall x_1, \dots, x_n \in M.\, (\varphi^M(x_1, \dots, x_n) \to \varphi^N(x_1, \dots, x_n)) \]
        \item \emph{downwards absolute} for \( M, N \) if
        \[ \forall x_1, \dots, x_n \in M.\, (\varphi^N(x_1, \dots, x_n) \to \varphi^M(x_1, \dots, x_n)) \]
        \item \emph{absolute} for \( M, N \) if it is both upwards and downwards absolute, or equivalently,
        \[ \forall x_1, \dots, x_n \in M.\, (\varphi^M(x_1, \dots, x_n) \leftrightarrow \varphi^N(x_1, \dots, x_n)) \]
    \end{enumerate}
\end{definition}
If \( N = \mathrm{V} \), we simply say that \( \varphi \) is (upwards or downwards) absolute for \( M \).
If \( \Gamma \) is a set of formulas, we say that \( \Gamma \) is (upwards or downwards) absolute for \( M, N \) if and only if \( \varphi \) is (upwards or downwards) absolute for \( M, N \) for each \( \varphi \in \Gamma \).
Suppose \( T \) is a set of sentences and \( f \) is a defined function by \( \varphi \).
Then for \( M \subseteq N \) models of \( T \), we say that \( f \) is absolute for \( M, N \) precisely when \( \varphi \) is absolute for \( M, N \).
\begin{example}
    If \( M \subseteq N \) both satisfy extensionality, then the empty set is absolute for \( M, N \) by the formula \( \forall x \in a.\, (x \neq x) \).
    The power set of \( 2 \) is not absolute between \( 4 \) and \( \mathrm{V} \), because in \( 4 \), it has only two elements.
\end{example}
\begin{example}
    \( \varphi \leftrightarrow \psi \) does not imply \( \varphi^M \leftrightarrow \psi^M \).
    Let \( \varphi(v) \) be the statement \( \forall x.\, (x \notin v) \); in \( \mathsf{ZF} \) this defines \( \varnothing \).
    Now, the following are two ways to express \( 0 \in z \).
    \[ \psi(z) \equiv \exists y.\, (\varphi(y) \wedge y \in z);\quad \theta(z) \equiv \forall y.\, (\varphi(y) \Rightarrow y \in z) \]
    Note that if there exists a unique \( y \) such that \( \varphi(y) \), then these are equivalent.
    However, this is often not the case, for example if
    \[ a = 0;\quad b = \qty{0};\quad c = \qty{\qty{\qty{0}}};\quad M = \qty{a, b, c} \]
    then \( \varphi^M(a) \) holds, so \( \psi^M(b) \), but \( \varphi^M(c) \) also holds, so \( \theta^M(b) \) fails.
\end{example}
The main obstacle to absoluteness for basic statements turns out to be transitivity of the model.
\begin{definition}
    Given classes \( M \subseteq N \), we say that \( M \) is \emph{transitive} in \( N \) if
    \[ \forall x, y \in N.\, (x \in M \wedge y \in x \Rightarrow y \in M) \]
\end{definition}

\subsection{The L\'evy hierarchy}
\begin{definition}
    The class of formulas \( \Delta_0 \) is the smallest class \( \Gamma \) closed under the following conditions.
    \begin{enumerate}
        \item if \( \varphi \) is atomic, \( \varphi \in \Gamma \) (that is, \( (v_i \in v_j) \in \Gamma \) and \( (v_i = v_j) \in \Gamma \));
        \item if \( \varphi, \psi \in \Gamma \), then \( \varphi \vee \psi \in \Gamma \) and \( \neg\varphi \in \Gamma \); and
        \item if \( \varphi \in \Gamma \), then \( (\forall v_i \in v_j.\, \varphi) \in \Gamma \) and \( (\exists v_i \in v_j.\, \varphi) \in \Gamma \).
    \end{enumerate}
\end{definition}
That is, \( \Delta_0 \) is the class of formulas generated from atomic formulas by Boolean operations and bounded quantification.
\begin{definition}
    We proceed by induction to define \( \Sigma_n \) and \( \Pi_n \) as follows.
    \begin{enumerate}
        \item \( \Sigma_0 = \Pi_0 = \Delta_0 \);
        \item if \( \varphi \) is \( \Pi_{n-1} \) then \( \exists v_i.\, \varphi \) is \( \Sigma_n \);
        \item if \( \varphi \) is \( \Sigma_{n-1} \) then \( \forall v_i.\, \varphi \) is \( \Pi_n \).
    \end{enumerate}
\end{definition}
\begin{example}
    The formula \( \forall v_1.\, \exists v_2.\, \forall v_3.\, (v_4 = v_3) \) is \( \Pi_3 \).
    But \( (\forall v_1.\, v_1 = v_2) \wedge v_3 = v_4 \) is not \( \Pi_n \) or \( \Sigma_n \) for any \( n \).
\end{example}
\begin{definition}
    Given an \( \mathcal L_\in \)-theory \( T \), let \( \Sigma_n^T \) be the class of formulas \( \Gamma \) such that for any \( \varphi \in \Gamma \), there exists \( \psi \in \Sigma_n \) such that \( T \vdash \varphi \leftrightarrow \psi \).
    We define \( \Pi_n^T \) analogously.
    A formula is in \( \Delta_n^T \) if there exists \( \psi \in \Sigma_n \) and \( \theta \in \Pi_n \) such that \( T \vdash \varphi \leftrightarrow \psi \) and \( T \vdash \varphi \leftrightarrow \theta \).
\end{definition}
Note that \( \Delta_n \) only makes much sense with respect to some theory \( T \) for \( n > 0 \).
\begin{lemma}
    If \( \varphi \) and \( \psi \) are in \( \Sigma_n^{\mathsf{ZF}} \), then so are
    \[ \exists v.\, \varphi;\quad \varphi \vee \psi;\quad \varphi \wedge \psi;\quad \exists v_i \in v_j.\, \varphi;\quad \forall v_i \in v_j.\, \varphi \]
    If \( \varphi \) is in \( \Sigma_n^{\mathsf{ZF}} \), then \( \neg\varphi \) is in \( \Pi_n^{\mathsf{ZF}} \).
    Further, for every \( \varphi \), there exists \( n \) such that \( \varphi \) is in \( \Sigma_n^{\mathsf{ZF}} \), and if \( \varphi \) is in \( \Sigma_n^{\mathsf{ZF}} \), then \( \varphi \) is in \( \Sigma_m^{\mathsf{ZF}} \) for all \( m \geq n \).
\end{lemma}
\begin{remark}
    \( \exists x_1.\, \forall x_2.\, \exists x_3.\, \forall y.\, (y \in v \to v \neq v) \) is \( \Sigma_4 \), but is logically equivalent to the statement \( \forall y \in v.\, v \neq v \), which is \( \Sigma_0 \).
    The fact that \( \Sigma_n^{\mathsf{ZF}} \) is closed under bounded quantification depends on the axiom of collection.
    In particular, in Zermelo set theory, there is a \( \Sigma_1^{\mathsf{Z}} \) formula \( \varphi \) such that \( \forall x \in a.\, \varphi \) is not \( \Sigma_1^{\mathsf{Z}} \).
    In intuitionistic logic, these classes are very badly behaved; for instance, we could have a \( \Pi_1^T \) formula \( \varphi \) such that \( \neg\varphi \) is not \( \Sigma_1^T \).
\end{remark}
We can now show absoluteness for \( \Delta_0 \) formulas between transitive models.
\begin{theorem}
    Let \( M \) be transitive in \( N \) and \( M \subseteq N \), and let \( \varphi(\vb u) \) be a \( \Delta_0 \)-formula.
    Then, for any \( \vb a \in M \),
    \[ M \vDash \varphi(\vb a) \text{ if and only if } N \vDash \varphi(\vb a) \]
\end{theorem}
\begin{proof}
    We prove this by induction on the class \( \Delta_0 \).
    The cases of atomic formulas and propositional connectives are immediate, so it suffices to show the result for \( \exists x \in a.\, \varphi \) where \( \varphi \) is absolute between \( M \) and \( N \).
    Suppose \( M \vDash \exists x \in a.\, \varphi(x) \), so there exists \( b \in M \) such that \( M \vDash b \in a \wedge \varphi(b) \).
    Then we also have \( N \vDash b \in a \wedge \varphi(b) \) by absoluteness of \( \varphi \), as required.
    Conversely, suppose \( N \vDash \exists x \in a.\, \varphi(x) \), so there exists \( b \in N \) such that \( N \vDash b \in a \wedge \varphi(b) \).
    Since \( M \) is transitive in \( N \), we obtain \( b \in M \), so \( M \vDash b \in a \wedge \varphi(b) \) by absoluteness of \( \varphi \).
    % TODO: remark on dropping parameters
\end{proof}
\begin{proposition}
    The following are \( \Delta_0^{\mathsf{ZF}} \), and therefore absolute between transitive models.
    \begin{enumerate}
        \item \( x \subseteq y \);
        \item \( a = \qty{x, y} \) (the unordered pair);
        \item \( a = \langle x, y \rangle \) (the ordered pair);
        \item \( a = x \times y \);
        \item \( a = \bigcup b \);
        \item \( a \) is a transitive set;
        \item \( x = \varnothing \);
        \item \( r \) is a relation;
        \item \( r \) is a function;
        \item \( r \) is a relation with domain \( a \) and range \( b \);
        \item \( x \) is the pointwise image of \( r \) on \( a \), denoted \( r '' a = \qty{y \mid \exists x \in a.\, \langle x, y \rangle \in r} \);
        \item \( \eval{r}_a \).
    \end{enumerate}
\end{proposition}
\begin{remark}
    The following are not absolute between transitive models, and thus not \( \Delta_0^{\mathsf{ZF}} \).
    \begin{enumerate}
        \item the cofinality function \( \alpha \mapsto \cf(\alpha) \);
        \item being a cardinal;
        \item \( \omega_1 \);
        \item \( y = \mathcal P(x) \).
    \end{enumerate}
\end{remark}
\begin{lemma}
    The statement that a given set \( a \) is finite is \( \Delta_1^{\mathsf{ZF}} \).
\end{lemma}
\begin{proposition}
    Let \( M \) be transitive in \( N \) and \( M \subseteq N \).
    Then \( \Sigma_1 \) formulas are upwards absolute between \( M \) and \( N \), and \( \Pi_1 \) formulas are downwards absolute between \( M \) and \( N \).
\end{proposition}
\begin{corollary}
    \( \Delta_1^{\mathsf{ZF}} \) formulas are absolute between transitive models.
\end{corollary}
\begin{lemma}
    (\( \mathsf{ZF} \))
    The statement that \( \alpha \) is an ordinal is absolute.
\end{lemma}
\begin{proof}
    First, note that \( \alpha \) is an ordinal in \( \mathsf{ZF} \) if and only if it is a transitive set of transitive sets.
    This can be written as
    \[ (\forall \beta \in \alpha.\, \forall \gamma \in \beta.\, \gamma \in \alpha) \wedge (\forall \beta \in \alpha.\, \forall \gamma \in \beta.\, \forall \delta \in \gamma.\, \delta \in \beta) \]
    which is \( \Delta_0 \), as required.
\end{proof}
We can give a slightly better rephrasing of this lemma.
\begin{lemma}
    The statement that \( r \) is a strict total ordering of \( a \) is \( \Delta_0 \).
\end{lemma}
\begin{proof}
    The statement that \( r \) is a transitive relation on \( a \) is that
    \[ \forall x y z \in a.\, (\langle x, y \rangle \in r \wedge \langle y, z \rangle \in r \to \langle x, z \rangle \in r) \]
    Trichotomy is
    \[ \forall x y \in a.\, (\langle x, y \rangle \in r \vee \langle y, x \rangle \in r \vee x = y) \]
    Irreflexivity is
    \[ \forall x \in a.\, \langle x, x \rangle \notin r \]
\end{proof}
\begin{corollary}
    The statement that \( x \) is a transitive set totally ordered by \( \in \) is \( \Delta_0 \), and thus ordinals are in fact \( \Delta_0 \).
\end{corollary}
\begin{lemma}
    (\( \mathsf{ZF} \))
    The statement that \( r \) is well-founded on \( a \) is \( \Delta_1^{\mathsf{ZF}} \).
\end{lemma}
\begin{proof}
    The \( \Pi_1 \) formula is
    \[ r \text{ is a relation on } a \wedge \qty[\forall X.\,(\exists x \in X.\, (z = z) \wedge X \subseteq a) \to \exists x \in X.\, \forall y \in X.\, \langle y, z \rangle \notin r] \]
    For the \( \Sigma_1 \) formula, we first show that a relation is well-founded on \( a \) if and only if there exists a function \( a \to \mathrm{Ord} \) such that \( \langle y, x \rangle \in r \) implies \( f(y) \in f(x) \).
    Suppose \( r \) is well-founded; we then define \( f : a \to \mathrm{Ord} \) by \( f(x) = \sup\qty{f(y) + 1 \mid \langle y, x \rangle \in r} \), and one can show that this satisfies the required property.
    For the other direction, let \( X \subseteq a \) be a nonempty subset, and consider the pointwise image \( f''X \).
    This has a minimal element \( \alpha \), then for any \( z \in X \), if \( f(z) = \alpha \) then for all \( y \in X \), we have \( f(y) \geq \alpha \), so \( \langle y, z \rangle \notin r \).
    We then define well-foundedness with a \( \Sigma_1 \) formula as follows.
    \[ \exists f.\, \qty(f \text{ is a function} \wedge \forall u \in \ran f.\, (u \in \mathrm{Ord}) \wedge \forall x y \in a.\, (\langle y, x \rangle \in r \to f(y) \in f(x))) \]
\end{proof}
\begin{proposition}
    The following are \( \Delta_0^{\mathsf{ZF}} \).
    \begin{enumerate}
        \item \( x \) is a limit ordinal;
        \item \( x \) is a successor ordinal;
        \item \( x \) is a finite ordinal;
        \item \( x = \omega \);
        \item \( x = n \) for any finite ordinal \( n \).
    \end{enumerate}
\end{proposition}
\begin{proposition}
    The following are \( \Pi_1^{\mathsf{ZF}} \) and hence downwards absolute between transitive models.
    \begin{enumerate}
        \item \( \kappa \) is a cardinal;
        \item \( \kappa \) is regular;
        \item \( \kappa \) is a limit cardinal;
        \item \( \kappa \) is a strong limit cardinal.
    \end{enumerate}
\end{proposition}
\begin{lemma}
    (\( \mathsf{ZF} \))
    % TODO: comment on what this annotation means
    Let \( W \) be a nonempty transitive class.
    Then the axioms of extensionality, empty set, and foundation all hold in \( W \).
\end{lemma}
\begin{proof}
    For extensionality, the relativisation of
    \[ \forall x.\, \forall y.\, (\forall z.\, (z \in x \leftrightarrow x \in y) \to x = y) \]
    to \( W \) is
    \[ \forall x \in W.\, \forall y \in W.\, (\forall z \in W.\, (z \in x \leftrightarrow x \in y) \to x = y) \]
    Suppose \( x \in W, y \in W \), but \( x \neq y \).
    Then by extensionality in the metatheory, without loss of generality we can fix \( z \in x \) with \( z \notin y \).
    But since \( W \) is transitive, we must have \( z \in W \), contradicting \( x = y \), as required.

    As \( W \) is nonempty, we can use foundation to fix \( x \in W \) such that \( x \cap W = \varnothing \).
    Since \( W \) is transitive, \( x \subseteq W \), and therefore \( x = \varnothing \in W \).
    Moreover, the statement that \( x = \varnothing \) is \( \Delta_0 \) and therefore absolute.

    % TODO: are we done yet?
\end{proof}
\begin{lemma}
    (\( \mathsf{ZF} \))
    Let \( W \) be a transitive class.
    Then
    \begin{enumerate}
        \item if for any pair \( x, y \in W \), the real pair set \( \qty{x, y} \) lies in \( W \), then the axiom of pairing holds in \( W \);
        \item if for any set \( x \in W \), the union \( \bigcup x \) lies in \( W \), then the axiom of union holds in \( W \);
        \item if \( \omega \in W \), then the axiom of infinity holds in \( W \);
        \item if, for every formula \( \varphi \) with free variables in \( \qty{x, a, v_1, \dots, v_n} \), we have
        \[ \forall a, v_1, \dots, v_n \in W.\, \qty{x \in a \mid \varphi^W(x, a, v_1, \dots, v_n)} \in W \]
        then the axiom of separation holds in \( W \);
        \item if, for every formula \( \varphi \) with free variables in \( \qty{x, y, a, v_1, \dots, v_n} \), for all \( a, v_1, \dots, v_n \in W \), if
        \[ \forall x \in a.\, \exists! y \in W.\, \varphi^W(x, y, a, v_1, \dots, v_n) \]
        then
        \[ \exists b \in W.\, \qty{y \mid \exists x \in a.\, \varphi^W(x, y, a, v_1, \dots, v_n)} \subseteq b \]
        then the axiom of replacement holds in \( W \);
        \item if, for every \( a \in W \), there exists \( b \in W \) such that \( \mathcal P(a) \cap W = b \), then the axiom of power set holds in \( W \).
    \end{enumerate}
\end{lemma}
\begin{corollary}
    (\( \mathsf{ZF} \))
    If \( W \) is a nonempty transitive class satisfying the conditions of the previous lemma, it is a model of \( \mathsf{ZF} \).
\end{corollary}

\subsection{Transfinite recursion}
\begin{definition}
    A relation \( R \) is \emph{set-like} on a class \( A \) if for all \( x \in A \), the collection of \( R \)-predecessors of \( x \) is a set.
\end{definition}
\begin{example}
    \( \in \) is set-like on \( \mathrm{V} \), but \( \ni \) is not set-like on \( \mathrm{V} \).
\end{example}
Let \( A \) be a class, and let \( \varphi \) be such that \( A = \qty{x \mid \varphi(x)} \).
Then \( A^W = \qty{x \mid \varphi^W(x)} \).
We say that \( A \) is absolute for \( W \) if \( A^W = A \cap W \).
Viewing a class relation \( R \subseteq \mathrm{V} \times \mathrm{V} \) as a collection of ordered pairs \( \qty{\langle x, y \rangle \mid \psi(x, y)} \), we have \( R^W = \qty{\langle x, y \rangle \mid \psi^W(x, y)} \), and say that \( R \) is absolute for \( W \) if \( R^W = R \cap W^2 \).
Observe that if \( R \) is a class function, we can only refer to the \emph{function} \( R^W \) if we first check that \( (\forall x.\, \exists! y.\, \varphi(x, y))^W \).
In this case, we have \( R^W : W \to W \), and we say that \( R \) is an absolute function for \( W \) iff \( R^W = \eval{R}_W \).

We briefly recall the transfinite recursion theorem.
\begin{theorem}
    Let \( R \) be a relation which is well-founded and set-like on a class \( A \).
    Let \( F : A \times \mathrm{V} \to \mathrm{V} \) be a class function.
    Given \( x \in A \), let \( \operatorname{pred}(A, x, R) = \qty{y \in A \mid y\mathrel{R}x} \) be the set of \( R \)-predecessors of \( x \) in \( A \).
    Then there is a unique function \( G : A \to \mathrm{V} \) such that for all \( x \in A \),
    \[ G(x) = F\qty(x, \eval{G}_{\operatorname{pred}(A, x, R)}) \]
\end{theorem}
We now prove the absoluteness of transfinite recursion.
\begin{theorem}
    Let \( R \) be a relation which is well-founded and set-like on a class \( A \).
    Let \( F : A \times \mathrm{V} \to \mathrm{V} \) be a class function, and let \( G : A \to \mathrm{V} \) be the unique function given by applying transfinite recursion to \( F \).
    Suppose that \( W \) is a transitive model of \( \mathsf{ZF} \), and suppose that the following hold.
    \begin{enumerate}
        \item \( A \) and \( F \) are absolute for \( W \);
        \item \( R \) is absolute for \( W \) and \( (\text{\( R \) is set-like on \( A \)})^W \);
        \item for all \( x \in W \), then \( \operatorname{pred}(A, x, R) \subseteq W \).
    \end{enumerate}
    Then \( G \) is absolute for \( W \).
\end{theorem}
\begin{proof}
    By absoluteness, \( A^W = A \cap W \) and \( R^W = R \cap W^2 \).
    Hence, every nonempty subset of \( A^W \) has an \( R^W \)-minimal element.
    In particular, \( (\text{\( R \) is well-founded on \( A \)})^W \).
    We can then apply transfinite recursion in \( W \) to define a unique function \( G^W : A^W \to W \) such that for all \( x \in A^W \),
    \[ G^W(x) = F^W\qty(x, \eval{G^W}_{\operatorname{pred}^W(A^W, x, R^W)}) \]
    To prove absoluteness for \( G \), it suffices to show that \( G^W = \eval{G}_{A^W} \).
    We show this by transfinite induction in \( W \).
    Suppose that for all \( y \mathrel{R} x \), we have \( G^W(y) = G(y) \).
    By absoluteness, (iii), and the inductive hypothesis, we obtain
    \[ G^W(x) = F^W\qty(x, \eval{G^W}_{\operatorname{pred}^W(A^W, x, R^W)}) = F\qty(x, \eval{G}_{\operatorname{pred}(A, x, R)}) = G(x) \]
\end{proof}
\begin{corollary}
    The following are absolute for transitive models of \( \mathsf{ZFC} \):
    \begin{enumerate}
        \item the rank function;
        \item the transitive closure of a set;
        \item the addition and multiplication operations of ordinal arithmetic.
    \end{enumerate}
\end{corollary}

\subsection{The reflection theorem}
In this subsection, we will not use choice.

Recall the Tarski--Vaught test: if \( \mathcal M \) is a substructure of \( \mathcal N \) with universes \( M \) and \( N \) respectively, then the following two statements are equivalent.
\begin{enumerate}
    \item \( \mathcal M \) is an elementary substructure of \( \mathcal N \);
    \item for any formula \( \varphi(v, \vb w) \) and \( \vb a \in M \), if there exists \( b \in N \) such that \( \mathcal N \vDash \varphi(b, \vb a) \), then there exists \( c \in M \) such that \( \mathcal M \vDash \varphi(c, \vb a) \).
\end{enumerate}
\begin{definition}
    A finite list of formulas \( \bm\varphi = \varphi_1, \dots, \varphi_n \) is said to be \emph{subformula closed} if every subformula of the \( \varphi_i \) is contained on the list.
\end{definition}
We can now state a version of the Tarski--Vaught test for classes.
\begin{lemma}
    Let \( \bm\varphi \) be a subformula closed list of formulas, and suppose \( W \subseteq Z \) are nonempty classes.
    Then the following two statements are equivalent.
    \begin{enumerate}
        \item each formula in \( \bm\varphi \) is absolute for \( W \) and \( Z \);
        \item whenever \( \varphi_i \) is of the form \( \exists x.\, \varphi_j(x, \vb y) \) where the free variables of \( \varphi_j \) are equal to \( x \) or contained in \( \vb y \), then
        \[ \forall \vb y \in W.\, \qty(\exists x \in Z.\, \varphi_j^Z(x, \vb y) \to \exists x \in W.\, \varphi_j^Z(x, \vb y)) \]
    \end{enumerate}
\end{lemma}
\begin{proof}
    \emph{(i) implies (ii).}
    Suppose that each formula in \( \bm\varphi \) is absolute.
    Let \( \varphi_i \) be of the form \( \exists x.\, \varphi_j(x, \vb y) \), and fix \( \vb y \in W \).
    Then \( \varphi_i^Z(\vb y) \) is \( \exists x \in Z.\, \varphi_j^Z(x, \vb y) \).
    If this holds, by absoluteness \( \varphi_i^W(\vb y) \) holds, so there is \( x \in W \) such that \( \varphi_j^W(x, \vb y) \).
    Finally, \( W \subseteq Z \) and absoluteness of \( \varphi_j \) gives \( \exists x \in W.\, \varphi_j^Z(x, \vb y) \).

    \emph{(ii) implies (i).}
    We show this by induction on the length of \( \varphi_i \).
    The result if \( \varphi_i \) is atomic or of the form \( \varphi_j \vee \varphi_k \) or \( \neg\varphi_j \) is immediate.
    Suppose \( \varphi_i \) is of the form \( \exists x.\, \varphi_j(x, \vb y) \), and fix \( \vb y \in W \).
    Then \( \varphi_i^Z(\vb y) \) is equivalent to the statement \( \exists x \in Z.\, \varphi_j^Z(x, \vb y) \).
    By (ii), this gives \( \exists x \in W.\, \varphi_j^Z(x, \vb y) \).
    Since \( W \subseteq Z \), the reverse implication is trivial.
    But \( \exists x \in W.\, \varphi_j^Z(x, \vb y) \) is equivalent to the statement that \( \varphi_i^W(\vb y) \) holds, as required.
\end{proof}
\begin{theorem}[reflection theorem]
    Let \( W \) be a nonempty class, and suppose that there is a class function \( F_W \) such that for any ordinal \( \alpha \), \( F_W(\alpha) = W_\alpha \in \mathrm{V} \).
    Suppose that
    \begin{enumerate}
        \item if \( \alpha < \beta \), then \( W_\alpha \subseteq W_\beta \);
        \item if \( \lambda \) is a limit ordinal, then \( W_\lambda = \bigcup_{\alpha < \lambda} W_\alpha \);
        \item \( W = \bigcup_{\alpha \in \mathrm{Ord}} W_\alpha \).
    \end{enumerate}
    Then for any finite list of formulas \( \bm\varphi = \varphi_1, \dots, \varphi_n \), \( \mathsf{ZF} \) proves that for every \( \alpha \) there is a limit ordinal \( \beta > \alpha \) such that the \( \varphi_i \) are absolute between \( W_\beta \) and \( W \).
\end{theorem}
One example of such a class function is \( W_\alpha = \mathrm{V}_\alpha \).
\begin{corollary}[Montague--L\'evy reflection]
    For any finite list of formulas \( \bm\varphi = \varphi_1, \dots, \varphi_n \), \( \mathsf{ZF} \) proves that for every \( \alpha \) there is a limit ordinal \( \beta > \alpha \) such that the \( \varphi_i \) are absolute for \( \mathrm{V}_\beta \).
\end{corollary}
We now prove the reflection theorem.
\begin{proof}
    Let \( \bm\varphi = \varphi_1, \dots, \varphi_n \) be a finite list of formulas.
    By extending the list and taking logical equivalences if necessary, we will assume that this list is subformula-closed and that there are no universal quantifiers.
    For \( i \leq n \), we will define a function \( G_i : \mathrm{Ord} \to \mathrm{Ord} \) as follows.
    If \( \varphi_i \) is of the form \( \exists x.\, \varphi_j(x, \vb y) \) where \( \vb y \) is a tuple of length \( k_i \), we will define a function \( F_i : W^{k_i} \to \mathrm{Ord} \) by setting
    \[ F_i(\vb y) = \begin{cases}
        0 & \text{if } \neg\exists x \in W.\, \varphi_j^W(x, \vb y) \\
        \eta & \text{where } \eta \text{ is the least ordinal such that } \exists x \in W_\eta.\, \varphi_j^W(x, \vb y)
    \end{cases} \]
    We set
    \[ G_i(\delta) = \sup\qty{F_i(\vb y) \mid y \in W_\delta^{k_i}} \]
    If \( \varphi_i \) is not of this form, we set \( G_i(\delta) = 0 \) for all \( \delta \).
    Finally, we let
    \[ K(\delta) = \max\qty{\delta + 1, G_1(\delta), \dots, G_n(\delta)} \]
    Note that the \( F_i \) work in an analogous way to Skolem functions, but does not require choice.
    The \( F_i \) are well-defined, and, using replacement in \( \mathrm{V} \), since \( W_\delta \) is a set, \( F_i '' W_\delta^{k_i} \) is also a set in \( \mathrm{V} \), so \( G_i \) and \( K \) are both defined and take values in \( \mathrm{Ord} \).
    Also, \( G_i \) is monotone: if \( \delta \leq \delta' \) then \( G_i(\delta) \leq G(\delta') \).

    We claim that for every \( \alpha \) there is a limit ordinal \( \beta > \alpha \) such that for all \( \delta < \beta \) and \( i \leq n \), we have \( G_i(\delta) < \beta \); that is, \( \beta \) is closed under this process of finding witnesses.
    Set \( \lambda_0 = \alpha \) and let \( \lambda_{t+1} = K(\lambda_t) \).
    Then we set \( \beta = \sup_{t \in \omega} \lambda_t \), which is a limit ordinal as it is the supremum of a strictly increasing sequence of ordinals.
    If \( \delta < \beta \), then \( \delta < \lambda_t \) for some \( t \), so \( G_i(\delta) \leq G_i(\lambda_t) \) by monotonicity, but \( G_i(\lambda_t) \leq K(\lambda_t) = \lambda_{t+1} < \beta \) as required.

    To complete the theorem, it suffices to consider \( \varphi_i \) of the form \( \exists x.\, \varphi_j(x, \vb y) \) by the Tarski--Vaught test for classes above.
    Fix \( \vb y \in W_\beta \), and suppose there exists \( x \in W \) such that \( \varphi_j^W(x, \vb y) \).
    Since \( \beta \) is a limit ordinal and \( \vb y \) is a finite sequence in \( W_\beta \), we must have \( \vb y \in W_\gamma \) for some \( \gamma < \beta \).
    Thus
    \[ 0 < F_i(\vb y) \leq G_i(\gamma) < \beta \]
    so by construction, there exists a witness \( x \in W_\beta \) such that \( \varphi_j^W(x, \vb y) \).
    Hence \( \bm\varphi \) is absolute between \( W_\beta \) and \( W \) as required.
\end{proof}
\begin{remark}
    This is a theorem scheme; for every choice of formulas \( \bm\varphi \), it is a theorem of \( \mathsf{ZF} \) that \( \bm\varphi \) are absolute for some \( \mathrm{V}_\beta \).
    We cannot prove that for every collection of formulas \( \bm\varphi \), for all ordinals \( \alpha \) there exists \( \beta > \alpha \) such that \( \bm\varphi \) is absolute for \( W_\beta, W \).
    Note that even if \( \bm\varphi \) is absolute for \( W_\beta \) and \( W \), we need not have \( {\bm\varphi}^{W_\beta} \).

    If \( \bm\varphi \) is any finite list of axioms of \( \mathsf{ZF} \), then there are arbitrarily large \( \beta \) such that \( \bm\varphi \) holds in \( \mathrm{V}_\beta \).
    If \( \beta \) is a limit ordinal, \( \mathrm{V}_\beta \vDash \mathsf{Z}(\mathsf{C}) \), so we may restrict our attention to instances of replacement.
\end{remark}
\begin{corollary}
    Let \( T \) be an extension of \( \mathsf{ZF} \) in \( \mathcal L_\in \), and let \( \varphi_1, \dots, \varphi_n \) be a finite list of axioms from \( T \).
    Then \( T \) proves that for every \( \alpha \) there exists \( \beta > \alpha \) such that \( \qty(\bigwedge_{i=1}^n \varphi_i)^{\mathrm{V}_\beta} \).
\end{corollary}
\begin{corollary}
    % TODO: do we really need metatheoretic ZFC?
    (\( \mathsf{ZFC} \))
    Let \( W \) be a class and let \( \varphi_1, \dots, \varphi_n \) be a finite list of formulas in \( \mathcal L_\in \).
    Then \( \mathsf{ZFC} \) proves that for every transitive \( x \subseteq W \), there exists some transitive \( y \supseteq x \) such that the \( \varphi_i \) are absolute between \( y \) and \( W \), and \( \abs{y} \leq \max\qty{w, \abs{x}} \).
\end{corollary}
Taking \( x = \omega \) and \( W = \mathrm{V} \) gives the following result.
\begin{corollary}
    Let \( T \) be any set of sentences in \( \mathcal L_\in \) such that \( T \vdash \mathsf{ZFC} \).
    Let \( \varphi_i, \dots, \varphi_n \in T \).
    Then \( T \) proves that there is a transitive set \( y \) of cardinality \( \aleph_0 \) such that \( \qty(\bigwedge_{i=1}^n \varphi_i)^y \).
\end{corollary}
\begin{corollary}
    Let \( T \) be any consistent set of sentences in \( \mathcal L_\in \) such that \( T \vdash \mathsf{ZF} \).
    Then \( T \) is not finitely axiomatisable.
    That is, for any finite set of sentences \( \Gamma \) in \( \mathcal L_\in \) such that \( T \vdash \Gamma \), there exists a sentence \( \varphi \) such that \( T \vdash \varphi \) but \( \Gamma \nvdash \varphi \).
\end{corollary}
This only holds for first-order theories; for example, G\"odel--Bernays set theory is finitely axiomatisable.
\begin{proof}
    Let \( \varphi_1, \dots, \varphi_n \) be a set of sentences such that \( T \vdash \bigwedge_{i=1}^n \varphi_i \).
    Suppose that \( \bigwedge_{i=1}^n \varphi_i \) proves every axiom of \( T \).
    By reflection, \( T \) proves that for every \( \alpha \) there is \( \beta > \alpha \) such that the \( \varphi_i \) hold in \( \mathrm{V}_\beta \) if and only if they hold in \( \mathrm{V} \).
    Since they hold in \( \mathrm{V} \), they must hold in some \( \mathrm{V}_\beta \).
    Fix \( \beta_0 \) to be the least ordinal such that \( \bigwedge_{i=1}^n \varphi_i^{\mathrm{V}_{\beta_0}} \).
    Then all of the axioms of \( T \) hold in \( \mathrm{V}_{\beta_0} \), so \( \mathrm{V}_{\beta_0} \vDash T \).
    Since \( T \) extends \( \mathsf{ZF} \), our basic absoluteness results hold, so in particular, if \( \alpha \in \mathrm{V}_{\beta_0} \) then
    \[ \mathrm{V}_\alpha^{\mathrm{V}_{\beta_0}} = \mathrm{V}_\alpha \cap \mathrm{V}_{\beta_0} = \mathrm{V}_\alpha \]
    So \( \mathrm{V}_\alpha \) is absolute for \( \mathrm{V}_{\beta_0} \).
    Note that \( T \) proves that there exists \( \alpha \) such that \( \bigwedge_{i=1}^n \varphi_i^{\mathrm{V}_\alpha} \), but as \( \mathrm{V}_{\beta_0} \) satisfies every axiom of \( T \), this must be true in \( \mathrm{V}_{\beta_0} \).
    That is, there must be \( \alpha < \beta_0 \) such that \( \bigwedge_{i=1}^n \varphi_i^{\mathrm{V}_\alpha} \).
    This contradicts minimality of \( \beta_0 \).
\end{proof}

\subsection{Cardinal arithmetic}
In this subsection, we will use the axiom of choice.
We recall the following basic definitions and results.
\begin{definition}
    The \emph{cardinality} of a set \( x \), written \( \abs{x} \) is the least ordinal \( \alpha \) such that there is a bijection \( x \to \alpha \).
\end{definition}
This definition only makes sense given the well-ordering principle.
\begin{definition}
    The cardinal arithmetic operations are defined as follows.
    Let \( \kappa, \lambda \) be cardinals.
    \begin{enumerate}
        \item \( \kappa + \lambda = \abs{0 \times \kappa \cup 1 \times \lambda} \);
        \item \( \kappa \cdot \lambda = \abs{\kappa \times \lambda} \);
        \item \( \kappa^\lambda = \abs{\kappa^\lambda} \), the cardinality of the set of functions \( \lambda \to \kappa \);
        \item \( \kappa^{<\lambda} = \sup\qty{\kappa^\alpha \mid \alpha < \lambda, \alpha \text{ a cardinal}} \).
    \end{enumerate}
\end{definition}
\begin{theorem}[Hessenberg]
    If \( \kappa, \lambda \) are infinite cardinals, then
    \[ \kappa + \lambda = \kappa \cdot \lambda = \max\qty{\kappa, \lambda} \]
\end{theorem}
\begin{lemma}
    If \( \kappa, \lambda, \mu \) are cardinals, then
    \[ \kappa^{\lambda + \mu} = \kappa^\lambda \cdot \kappa^\mu;\quad (\kappa^\lambda)^\mu = \kappa^{\lambda \cdot \mu} \]
\end{lemma}
\begin{definition}
    A map between ordinals \( \alpha \to \beta \) is \emph{cofinal} if \( \sup \ran f = \beta \).
    The \emph{cofinality} of an ordinal \( \gamma \), written \( \cf(\gamma) \), is the least ordinal that admits a cofinal map to \( \gamma \).
    A limit ordinal \( \gamma \) is \emph{singular} if \( \cf(\gamma) < \gamma \), and \emph{regular} if \( \cf(\gamma) = \gamma \).
\end{definition}
\begin{remark}
    \begin{enumerate}
        \item Since the identity map is always cofinal, we have \( \cf(\gamma) \leq \gamma \).
        \item \( \omega = \cf(\omega) = \cf(\omega + \omega) = \cf(\aleph_\omega) \).
        \item \( \cf(\gamma) \leq \abs{\gamma} \).
    \end{enumerate}
\end{remark}
\begin{theorem}
    Let \( \gamma \) be a limit ordinal.
    Then
    \begin{enumerate}
        \item if \( \gamma \) is regular, \( \gamma \) is a cardinal;
        \item the cardinal successor \( \gamma^+ \) is a regular cardinal;
        \item \( \cf(\cf(\gamma)) = \cf(\gamma) \), so \( \cf(\gamma) \) is regular;
        \item \( \aleph_\alpha \) is regular whenever \( \alpha = 0 \) or a successor;
        \item if \( \lambda \) is a limit ordinal, \( \cf(\aleph_\lambda) = \cf(\lambda) \).
    \end{enumerate}
\end{theorem}
\begin{theorem}
    Let \( \kappa \) be a regular cardinal.
    If \( \mathcal F \) is a family of sets with \( \abs{\mathcal F} < \kappa \) and each \( \abs{X} < \kappa \) for \( X \in \mathcal F \), then \( \abs{\bigcup \mathcal F} < \kappa \).
\end{theorem}
\begin{proof}
    We show this by induction on \( \abs{\mathcal F} = \gamma < \kappa \).
    Suppose the claim holds for \( \gamma \), and consider \( \mathcal F = \qty{X_\alpha \mid \alpha < \gamma + 1} \).
    Then, assuming the sets involved are infinite,
    \[ \abs{\bigcup \mathcal F} = \abs{\bigcup_{\alpha < \gamma} X_\alpha \cup X_\gamma} = \abs{\bigcup_{\alpha < \gamma} X_\alpha} + \abs{X_\gamma} = \max\qty{\abs{\bigcup_{\alpha < \gamma} X_\alpha}, \abs{X_\gamma}} < \kappa \]
    Now suppose \( \gamma \) is a limit, and suppose the claim holds for all \( \beta < \gamma \).
    Let \( \mathcal F = \qty{X_\alpha \mid \alpha < \gamma} \), and define \( g : \gamma \to \kappa \) by
    \[ g(\beta) = \abs{\bigcup_{\alpha < \beta} X_\beta} \]
    But \( \kappa \) is regular and \( \gamma < \kappa \), so this map is not cofinal.
    Hence \( g '' \gamma = \abs{\bigcup \mathcal F} < \kappa \).
\end{proof}
We can generalise the notions of cardinal sum and product as follows.
\begin{definition}
    Let \( (\kappa_i)_{i \in I} \) be an indexed sequence of cardinals, and let \( (X_i)_{i \in I} \) be a sequence of pairwise disjoint sets with \( \abs{X_i} = \kappa_i \) for all \( i \in I \).
    Then the \emph{cardinal sum} of \( (\kappa_i) \) is
    \[ \sum_{i \in I} \kappa_i = \abs{\bigcup_{i \in I} X_i} \]
    The \emph{cardinal product} is
    \[ \prod_{i \in I} \kappa_i = \abs{\prod_{i \in I} X_i} \]
    where \( \prod_{i \in I} X_i \) denotes the set of functions \( f : I \to \bigcup_{i \in I} X_i \) such that \( f(i) \in X_i \) for each \( i \).
\end{definition}
The following theorem generalises Cantor's diagonal argument.
\begin{theorem}[K\"onig's theorem]
    Let \( I \) be an indexing set, and suppose that \( \kappa_i < \lambda_i \) for all \( i \in I \).
    Then
    \[ \sum_{i \in I} \kappa_i < \prod_{i \in I} \lambda_i \]
\end{theorem}
\begin{proof}
    Let \( (B_i)_{i \in I} \) be a sequence of disjoint sets with \( \abs{B_i} = \lambda_i \), and let \( B = \prod_{i \in I} B_i \).
    It suffices to show that for any sequence \( (A_i)_{i \in I} \) of subsets of \( B \) such that for all \( i \in I \), \( \abs{A_i} = \kappa_i \), then
    \[ \bigcup_{i \in I} A_i \neq B \]
    Given such a sequence, we let \( S_i \) be the projection of \( A_i \) onto its \( i \)th coordinate.
    \[ S_i = \qty{f(i) \mid f \in A_i} \]
    Then by definition, \( S_i \subseteq B_i \), and
    \[ \abs{S_i} \leq \abs{A_i} = \kappa_i < \lambda_i = \abs{B_i} \]
    Fix \( t_i \in B_i \setminus S_i \).
    Finally, we define \( g \in B \) by \( g(i) = t_i \); by construction, we have \( g \notin A_i \) for all \( i \), so \( g \in B \) but \( g \notin \bigcup_{i \in I} A_i \).
\end{proof}
\begin{corollary}
    If \( \kappa \geq 2 \) and \( \lambda \) is infinite, then
    \[ \kappa^\lambda > \lambda \]
\end{corollary}
\begin{proof}
    \[ \lambda = \sum_{\alpha < \lambda} 1 < \prod_{\alpha < \lambda} 2 = 2^\lambda \leq \kappa^\lambda \]
\end{proof}
\begin{corollary}
    \( \cf(2^\lambda) > \lambda \).
\end{corollary}
\begin{proof}
    Let \( f : \lambda \to 2^\lambda \), we show that \( \abs{\bigcup f '' \lambda} < 2^\lambda \).
    Since for all \( i \in I \), we have \( f(i) < 2^\lambda \), we deduce
    \[ \abs{\bigcup f '' \lambda} \leq \sum_{i < \lambda} \abs{f(i)} < \prod_{i < \lambda} 2^\lambda = (2^\lambda)^\lambda = 2^{\lambda \cdot \lambda} = 2^\lambda \]
\end{proof}
\begin{corollary}
    \( 2^{\aleph_0} \neq \kappa \) for any \( \kappa \) of cofinality \( \aleph_0 \).
    In particular, \( 2^{\aleph_0} \neq \aleph_\omega \).
\end{corollary}
\begin{corollary}
    \( \kappa^{\cf(\kappa)} > \kappa \) for every infinite cardinal \( \kappa \).
\end{corollary}
We can prove very little in general about cardinal exponentiation given \( \mathsf{ZFC} \).
\begin{definition}
    The \emph{generalised continuum hypothesis} is the statement that \( 2^\kappa = \kappa^+ \) for every infinite cardinal \( \kappa \).
    Equivalently, \( 2^{\aleph_\alpha} = \aleph_{\alpha + 1} \).
\end{definition}
Under this assumption, we can show the following.
\begin{theorem}
    (\( \mathsf{ZFC} + \mathsf{GCH} \))
    Let \( \kappa, \lambda \) be infinite cardinals.
    \begin{enumerate}
        \item if \( \kappa < \lambda \), then \( \kappa^\lambda = \lambda^+ \);
        \item if \( \cf(\kappa) \leq \lambda < \kappa \), then \( \kappa^\lambda = \kappa^+ \);
        \item if \( \lambda < \cf(\kappa) \), then \( \kappa^\lambda = \kappa \).
    \end{enumerate}
\end{theorem}
When we construct models with certain properties of cardinal arithmetic, we will often want to start with a model satisfying \( \mathsf{GCH} \) so that we have full control over cardinal exponentiation.
Without this assumption, we know much less.
The following theorems are essentially the only restrictions that we have on regular cardinals that are provable in \( \mathsf{ZFC} \).
\begin{theorem}
    Let \( \kappa, \lambda \) be cardinals.
    Then
    \begin{enumerate}
        \item if \( \kappa < \lambda \), then \( 2^\kappa \leq 2^\lambda \);
        \item \( \cf(2^\kappa) > \kappa \);
        \item if \( \kappa \) is a limit cardinal, then \( 2^\kappa = (2^{<\kappa})^{\cf(\kappa)} \).
    \end{enumerate}
\end{theorem}
\begin{theorem}
    Let \( \kappa, \lambda \) be infinite cardinals.
    Then
    \begin{enumerate}
        \item if \( \kappa \leq \lambda \), then \( \kappa^\lambda = 2^\lambda \);
        \item if \( \mu < \kappa \) is such that \( \mu^\lambda \geq \kappa \), then \( \kappa^\lambda = \mu^\lambda \);
        \item if \( \kappa > \lambda \) and \( \mu^\lambda < \kappa \) for all \( \mu < \kappa \), then
        \begin{enumerate}
            \item if \( \cf(\kappa) > \lambda \), then \( \kappa^\lambda = \kappa \);
            \item if \( \cf(\kappa) \leq \lambda \), then \( \kappa^\lambda = \kappa^{\cf(\kappa)} \).
        \end{enumerate}
    \end{enumerate}
\end{theorem}
\begin{theorem}[Silver]
    Suppose that \( \kappa \) is a singular cardinal such that \( \cf(\kappa) > \aleph_0 \) and \( 2^\alpha = \alpha^+ \) for all \( \alpha < \kappa \).
    Then \( 2^\kappa = \kappa^+ \).
\end{theorem}
This theorem therefore states that the generalised continuum hypothesis cannot first break at a singular cardinal with cofinality larger than \( \aleph_0 \).
\begin{remark}
    It is consistent (relative to large cardinals, such as a measurable cardinal) to have \( 2^{\aleph_n} = \aleph_{n + 1} \) for all \( n \in \omega \), but \( 2^{\aleph_\omega} = \aleph_{\omega + 2} \).
\end{remark}
\begin{theorem}[Shelah]
    Suppose that \( 2^{\aleph_n} < \aleph_\omega \) for all \( n \in \omega \), so \( \aleph_\omega \) is a strong limit cardinal.
    Then \( 2^{\aleph_\omega} < \aleph_{\omega_4} \).
\end{theorem}
It is not known if this bound can be improved, but it is conjectured that \( 2^{\aleph_\omega} < \aleph_{\omega_1} \).
